$\forall$$X$:Type, $x$:chain\_config(), ${\it head}$, ${\it tail}$:$X$, ${\it pred}$:(Id$\rightarrow$$X$), ${\it succ}$:(Id$\rightarrow\mathbb{N}\rightarrow$$X$).
\\[0ex]chain\_config\_ind($x$;${\it head}$;${\it tail}$;${\it id}$.${\it pred}$(${\it id}$);${\it id}$,${\it num}$.${\it succ}$(${\it id}$,${\it num}$)) $\in$ $X$